Special Relations

Special Binary Relations

Binary relations that are partial orders, linear orders, tree orders, and piece-wise linear orders can be axiomatized using first order quantifiers. However, reasoning with these quantified axioms involves non-linear overhead, up to a quadratic number of quantifier instantiations. The decision procedures for partial, linear, tree and piece-wise linear orders in z3 use variants of Ford-Fulkerson push relabeling graphs.

Partial Order

Use instead

(define-fun R ((x A) (y A)) Bool ((_ partial-order 0) x y))

We are using the index 0 to identify the partial order relation R. To create a different relation that is also a partial order use a different index, such as (_ partial-order 1).

Linear Order

Use instead

Tree Order

Use instead

Piece-wise Linear Order

Use instead

(define-fun R ((x A) (y A)) Bool ((_ piecewise-linear-order 0) x y))

Transitive Closures

The transitive closure of a relation is not first-order axiomatizable. However, the decision problem for ground formulas is decidable because for every binary relation R over a finite domain, the transitive closure of it is defined over the finite graph of R. The small model property contrasts non-ground first-order formulas using transitive closure that are not first-order axiomatizable.